$\forall$$T$:Type. 
\\[0ex]subtype\_rel($T$; $\mathbb{Z}$) $\Rightarrow$ ($\forall$${\it bs}$,${\it as}$:($T$ List), $x$:$T$. ($x$ $\in$ merge(${\it as}$; ${\it bs}$)) $\Leftarrow\!\Rightarrow$ (($x$ $\in$ ${\it as}$) $\vee$ ($x$ $\in$ ${\it bs}$)))